x, tg:Id, k:Knd, l:IdLnk, T, A, B:Type, f:(AB(T List)), es:ES.
sends k(v:B) on l:
tagged([<tg, s,v. f(s(x),v)>],State(x : A),v):if isrcv(k) then tg : T  tag(k) : B else tg : T fi 
 sends1-p(es;x;A;k;B;l;tg;T;f) 

latex

Definitions

, t  T, A c B, P  Q, Top, x:A. B(x), P & Q, ff, tt, SQType(T), {T}, if b then t else f fi , x. t(x), xL. P(x), True, T, i  j < k, {i..j}, S  T, P  Q, P  Q, t.2, f o g, DeclaredType(ds;x), t.1, A, x(s), Unit, , rcvs from e on l = L, Y, reduce(f;k;as), (state when e), sends-msgs(s;v;tg_f), concat(ll), , (x  l), x:A. B(x), A  B, False,

Lemmas

rcv wf, es-E wf, lsrc wf, es-loc wf, es-kind wf, eqof eq btrue, id-deq wf, fpf-cap-single, not wf, bnot wf, assert wf, bool wf, fpf-cap-single1, deq wf, subtype rel self, fpf-cap-single-join, isrcv wf, es-tag wf, Id sq, es-kind-rcv, subtype rel set, top wf, assert of bnot, eqff to assert, iff transitivity, tagof wf, fpf-single wf, fpf-join wf, eqtt to assert, fpf-dom wf, es-lnk wf, subtype rel list, l member wf, es-rcv-kind, es-val wf, es-vartype wf, es-when wf, map wf, append nil sq, length-map-sq, Id wf, fpf-cap wf, length wf1, le wf, squash wf, select wf, select-map, length wf nat, pi1 wf, pi2 wf, event system wf, es-isrcv wf, list-set-type2, es-sender wf, map-map, map-id, decl-type wf, member map, es-locl wf, l before wf, iff wf